During the design of a digital integrated circuit, a register transfer level (RTL) design is often used as a higher-level representation of the circuit. The RTL behavior of the circuit may be described with a hardware description language, such as Verilog. Once the RTL design is finalized, a lower, transistor-level representation may be derived from the RTL, often automatically. For the circuit to operate as intended, it is important to ensure that the lower, transistor-level model exhibits the desired behavior and functionality as specified via the higher-level RTL model.
Formal equivalence verification (FEV) is a process used to ensure correct implementation of integrated circuit designs by asserting that two representations of a circuit design exhibit equivalent behavior. FEV may be used to verify equivalence between the implementation (e.g., lower, transistor-level design) and specification (e.g., higher-level RTL). FEV may also be used when design changes are introduced, to ensure functional equivalence between the modified circuit model and the original circuit model. Formal property verification (FPV) process, on the other hand, is utilized to verify the functional correctness of properties specified on any given model of an integrated circuit design.
FEV compares the functional behavior of two models at a set of verification points, whereas FPV verifies the functional behavior of a model at a set of verification points. The number of verification points for FEV and/or FPV depends on the design size and complexity of a circuit, but it is usually very large. An integrated circuit design model may sometimes contain over 100,000 verification points. Checking such a large number of verification points may negatively impact the capacity and runtime of the verification process, and may also increase the user debug time.